\documentclass[12pt]{report}
\usepackage[]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{fullpage}
\usepackage{coqdoc}
\usepackage{amsmath,amssymb}
\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% This file has been automatically generated with the command
%% coqdoc -q -g --latex -o MatrixEval.tex MatrixEval.v 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\coqlibrary{MatrixEval}{Library }{MatrixEval}

\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Inductive} \coqdocvar{MatrixEval} (\coqdocvar{s}: \coqdocvar{State})(\coqdocvar{m} \coqdocvar{n}: \coqdocvar{Integer}) : \coqdocvar{MatrixExp} \ensuremath{\rightarrow} \coqdocvar{Matrix} \coqdocvar{Byte} \coqdocvar{m} \coqdocvar{n} \ensuremath{\rightarrow} \coqdockw{Prop} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{matrix\_eval\_lit} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{mx}:\coqdocvar{Matrix} \coqdocvar{Byte} \coqdocvar{m} \coqdocvar{n}),\coqdoceol
\coqdocindent{3.00em}
\coqdocvar{MatrixEval} \coqdocvar{s} (\coqdocvar{matrix\_exp\_lit} \coqdocvar{mx}) \coqdocvar{mx}\coqdoceol
\coqdocindent{1.00em}
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{matrix\_eval\_id} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{i}:\coqdocvar{Id})(\coqdocvar{mx}:\coqdocvar{Matrix} \coqdocvar{Byte} \coqdocvar{m} \coqdocvar{n}),\coqdoceol
\coqdocindent{2.00em}
\coqdocvar{s} \coqdocvar{i} = \coqdocvar{Some} (\coqdocvar{byte\_matrix\_val} \coqdocvar{mx}) \ensuremath{\rightarrow} \coqdocvar{MatrixEval} \coqdocvar{s} (\coqdocvar{matrix\_exp\_id} \coqdocvar{i}) \coqdocvar{mx}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{matrix\_eval\_init} : \coqdockw{\ensuremath{\forall}} \coqdocvar{aexp1} \coqdocvar{aexp2} \coqdocvar{a},\coqdoceol
\coqdocindent{12.00em}
\coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{aexp1} \coqdocvar{m} \ensuremath{\rightarrow} \coqdocvar{ArithEval} \coqdocvar{s} \coqdocvar{aexp2} \coqdocvar{n} \ensuremath{\rightarrow}\coqdoceol
\coqdocindent{12.00em}
\coqdocvar{MatrixEval} \coqdocvar{s} (\coqdocvar{matrix\_exp\_init} \coqdocvar{aexp1} \coqdocvar{aexp2}) (\coqdocvar{matrix\_zero} \coqdocvar{a} \coqdocvar{m} \coqdocvar{n})\coqdoceol
\coqdocnoindent
.\coqdoceol
\end{coqdoccode}
\end{document}
